$\forall$${\it es}$:ES, $i$, $x$:Id, $T$:Type, $v$:$T$.
\\[0ex]($\uparrow$discrete($i$;$x$)) $\Rightarrow$ @$i$ continuous $x$ initially $\lambda$$t$.$v$:$T$ $\Rightarrow$ @$i$ $x$ initially $v$:$T$